Inference at * 1 
Iof proof for Lemma adjacent-cons:



1. T : Type
2. x : T
3. y : T
4. u : T
5. L : T List
6. i : {0..((||L||+1) - 1)}
7. x = [u / L][i]
8. y = [u / L][(i+1)]
9. 0 < ||L||
  (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)])) 

latex

 by CaseNat 0 `i' 

latex

 1: 

 1: 10. i = 0
 1:   (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)]))
 2: 

 2: 10. (i = 0)
 2:   (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)]))
 .

Definitions	(xL.P(x)), xL. P(x), |r|, x f y, f(a), A c B, a < b, |g|, a <p b, a  b, |p|, a ~ b, b | a, x:A. B(x), x:A  B(x), x,y:A//B(x;y), b, , Atom, Dec(P), P  Q, left + right, {x:A| B(x)} , i  j < k, A  B, P & Q, A, False, s ~ t, n - m, ||as||, n+m, #$n, l[i], [car / cdr], , t  T, a < b, s = t, type List, Type, SQType(T), x:A. B(x), P  Q, x:AB(x), {T}, , {i..j}
Lemmas	decidable int equal, guard wf